skip to main content
10.1145/2382196.2382271acmconferencesArticle/Chapter ViewAbstractPublication PagesccsConference Proceedingsconference-collections
research-article

Computational verification of C protocol implementations by symbolic execution

Published:16 October 2012Publication History

ABSTRACT

We verify cryptographic protocols coded in C for correspondence properties with respect to the computational model of cryptography. The first step uses symbolic execution to extract a process calculus model from a C implementation of the protocol. The new contribution is the second step in which we translate the extracted model to a CryptoVerif protocol description, such that successful verification with CryptoVerif implies the security of the original C implementation. We implement our method and apply it to verify several protocols out of reach of previous work in the symbolic model (using ProVerif), either due to the use of XOR and Diffie-Hellman commitments, or due to the lack of an appropriate computational soundness result. We analyse only a single execution path, so our tool is limited to code following a fixed protocol narration. This is the first security analysis of C code to target a verifier for the computational model. We successfully verify over 3000 LOC. One example (about 1000 LOC) is independently written and currently in testing phase for industrial deployment; during its analysis we uncovered a vulnerability now fixed by its author.

References

  1. M. Abadi, B. Blanchet, and H. Comon-Lundh. Models and proofs of protocol security: A progress report. In A. Bouajjani and O. Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 35--49. Springer, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  2. M. Abadi and P. Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). J. Cryptology, 15(2):103--127, 2002.Google ScholarGoogle ScholarDigital LibraryDigital Library
  3. M. Abe and V. D. Gligor, editors. Proceedings of the 2008 ACM Symposium on Information, Computer and Communications Security, ASIACCS 2008, Tokyo, Japan, March 18--20, 2008. ACM, 2008. Google ScholarGoogle ScholarCross RefCross Ref
  4. M. Aizatulin, F. Dupressoir, A. D. Gordon, and J. Jürjens. Verifying cryptographic code in C: Some experience and the Csec challenge. In Formal Aspects of Security and Trust (FAST 2011), Lecture Notes in Computer Science. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  5. M. Aizatulin, A. D. Gordon, and J. Jürjens. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011. Full version available at http://arxiv.org/abs/1107.1017. Google ScholarGoogle ScholarDigital LibraryDigital Library
  6. M. Aizatulin, A. D. Gordon, and J. Jürjens. Computational verification of C protocol implementations by symbolic execution. Technical Report MSR-TR-2012-80, Microsoft Research, 2012.Google ScholarGoogle ScholarDigital LibraryDigital Library
  7. M. Backes, D. Hofheinz, and D. Unruh. CoSP: A general framework for computational soundness proofs. In ACM Conference on Computer and Communications Security, pages 66--78, 2009. Preprint on IACR ePrint 2009/080. Google ScholarGoogle ScholarDigital LibraryDigital Library
  8. M. Backes, M. Maffei, and D. Unruh. Computationally sound verification of source code. In CCS, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  9. M. Barbosa, J. Pinto, J. Filliâtre, and B. Vieira. A deductive verification platform for cryptographic software. In Proceedings of the Fourth International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2010), volume 33 of Electronic Communications of the EASST. EASST, 2010.Google ScholarGoogle Scholar
  10. G. Barthe, B. Grégoire, S. Heraud, and S. Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology -- CRYPTO 2011, Lecture Notes in Computer Science. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  11. J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. Refinement types for secure implementations. In CSF '08: Proceedings of the 2008 21st IEEE Computer Security Foundations Symposium, pages 17--32. IEEE Computer Society, 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  12. K. Bhargavan, R. Corin, C. Fournet, and E. Zalinescu. Automated computational verification for cryptographic protocol implementations. Unpublished draft, Oct. 2009.Google ScholarGoogle Scholar
  13. K. Bhargavan, C. Fournet, R. Corin, and E. Zalinescu. Cryptographically verified implementations for TLS. In CCS '08: Proceedings of the 15th ACM conference on Computer and communications security, pages 459--468, Alexandria, VA, Oct. 2008. ACM. Google ScholarGoogle ScholarDigital LibraryDigital Library
  14. K. Bhargavan, C. Fournet, and A. D. Gordon. Modular verification of security protocol code by typing. In ACM Symposium on Principles of Programming Languages (POPL'10), pages 445--456, 2010. Google ScholarGoogle ScholarDigital LibraryDigital Library
  15. K. Bhargavan, C. Fournet, A. D. Gordon, and N. Swamy. Verified implementations of the information card federated identity-management protocol. In Abe and Gligor {3}, pages 123--135. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. K. Bhargavan, C. Fournet, A. D. Gordon, and S. Tse. Verified interoperable implementations of security protocols. In CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations, pages 139--152. IEEE Computer Society, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  17. B. Blanchet. An efficient cryptographic protocol verifier based on prolog rules. In CSFW, pages 82--96. IEEE Computer Society, 2001. Google ScholarGoogle ScholarDigital LibraryDigital Library
  18. B. Blanchet. Computationally sound mechanized proofs of correspondence assertions. In 20th IEEE Computer Security Foundations Symposium (CSF'07), pages 97--111, Venice, Italy, July 2007. IEEE. Google ScholarGoogle ScholarDigital LibraryDigital Library
  19. B. Blanchet. A computationally sound mechanized prover for security protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193--207, Oct.-Dec. 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  20. B. Blanchet, A. D. Jaggard, A. Scedrov, and J.-K. Tsay. Computationally sound mechanized proofs for basic and public-key kerberos. In Abe and GligorciteDBLP:conf/ccs/2008asia, pages 87--99. Google ScholarGoogle ScholarDigital LibraryDigital Library
  21. C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In USENIX Symposium on Operating Systems Design and Implementation (OSDI 2008), San Diego, CA, Dec. 2008. Google ScholarGoogle ScholarDigital LibraryDigital Library
  22. D. Cadé and B. Blanchet. From computationally-proved protocol specifications to implementations. In International Conference on Availability, Reliability and Security (ARES 2012), 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  23. S. Chaki and A. Datta. ASPIER: An automated framework for verifying security protocol implementations. In Computer Security Foundations Workshop, pages 172--185, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  24. R. Corin and F. A. Manzano. Efficient symbolic execution for analysing cryptographic protocol implementations. In International Symposium on Engineering Secure Software and Systems (ESSOS'11), LNCS. Springer, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  25. V. Cortier, S. Kremer, and B. Warinschi. A survey of symbolic methods in computational analysis of cryptographic systems. J. Autom. Reasoning, 46(3--4):225--259, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  26. D. Dolev and A. Yao. On the Security of Public-Key Protocols. IEEE Transactions on Information Theory, 29(2):198--208, 1983. Google ScholarGoogle ScholarDigital LibraryDigital Library
  27. F. Dupressoir, A. D. Gordon, J. Jürjens, and D. A. Naumann. Guiding a general-purpose C verifier to prove cryptographic protocols. In 24th IEEE Computer Security Foundations Symposium, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  28. B. Dutertre and L. D. Moura. The Yices SMT Solver. Technical report, Computer Science Laboratory, SRI International, 2006.Google ScholarGoogle Scholar
  29. C. Fournet, K. Bhargavan, and A. D. Gordon. Cryptographic verification by typing for a sample protocol implementation. In Foundations of Security and Design VI (FOSAD 2010), Lecture Notes in Computer Science. Springer, 2011. To appear. Google ScholarGoogle ScholarDigital LibraryDigital Library
  30. C. Fournet, M. Kohlweiss, and P.-Y. Strub. Modular code-based cryptographic verification. In 18th ACM Conference on Computer and Communications Security (CCS 2011), 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. http://frama-c.cea.fr/, 2009.Google ScholarGoogle Scholar
  32. P. Godefroid and S. Khurshid. Exploring very large state spaces using genetic algorithms. In Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), volume 2280, pages 266--280. Springer, 2002. Google ScholarGoogle ScholarDigital LibraryDigital Library
  33. P. Godefroid, N. Klarlund, and K. Sen. DART: directed automated random testing. In Programming Language Design and Implementation (PLDI'05), pages 213--223. ACM, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  34. S. Goldwasser and S. Micali. Probabilistic encryption. Journal of Computer and System Science, 28(2):270--299, 1984.Google ScholarGoogle ScholarCross RefCross Ref
  35. A. D. Gordon. Provable implementations of security protocols. In LICS, pages 345--346, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  36. J. Goubault-Larrecq and F. Parrennes. Cryptographic protocol analysis on real C code. In Proceedings of the 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), volume 3385 of Lecture Notes in Computer Science, pages 363--379. Springer, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  37. P. Gupta and V. Shmatikov. Towards computationally sound symbolic analysis of key exchange protocols. In V. Atluri, P. Samarati, R. Küsters, and J. C. Mitchell, editors, FMSE, pages 23--32. ACM, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  38. C. Hritcu. Union, Intersection, and Refinement Types and Reasoning About Type Disjointness for Security Protocol Analysis. PhD thesis, Department of Computer Science, Saarland University, 2011.Google ScholarGoogle Scholar
  39. A. Jeffrey and R. Ley-Wild. Dynamic model checking of C cryptographic protocol implementations. In Proceedings of Workshop on Foundations of Computer Security and Automated Reasoning for Security Protocol Analysis, 2006.Google ScholarGoogle Scholar
  40. J. C. King. Symbolic execution and program testing. Commun. ACM, 19(7):385--394, 1976. Google ScholarGoogle ScholarDigital LibraryDigital Library
  41. R. Küsters and T. Truderung. Reducing protocol analysis with XOR to the XOR-free case in the horn theory based approach. Journal of Automated Reasoning, 46(3):325--352, 2011. Google ScholarGoogle ScholarDigital LibraryDigital Library
  42. R. Küsters, T. Truderung, and J. Graf. A Framework for the Cryptographic Verification of Java-like Programs. In IEEE Computer Security Foundations Symposium, CSF 2012. IEEE Computer Society, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  43. R. Küsters and M. Tuengerthal. Computational soundness for key exchange protocols with symmetric encryption. In E. Al-Shaer, S. Jha, and A. D. Keromytis, editors, ACM Conference on Computer and Communications Security, pages 91--100. ACM, 2009. Google ScholarGoogle ScholarDigital LibraryDigital Library
  44. P. Lincoln, J. C. Mitchell, M. Mitchell, and A. Scedrov. Probabilistic polynomial-time equivalence and security analysis. In J. M. Wing, J. Woodcock, and J. Davies, editors, World Congress on Formal Methods, volume 1708 of Lecture Notes in Computer Science, pages 776--793. Springer, 1999. Google ScholarGoogle ScholarDigital LibraryDigital Library
  45. G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In Proceedings of the 11th International Conference on Compiler Construction, CC '02, pages 213--228, London, UK, 2002. Springer-Verlag. Google ScholarGoogle ScholarDigital LibraryDigital Library
  46. PolarSSL. http://polarssl.org.Google ScholarGoogle Scholar
  47. N. Polikarpova and M. Moskal. Verifying implementations of security protocols by refinement. In Verified Software: Theories, Tools and Experiments (VSTTE 2012), volume 7152 of Lecture Notes in Computer Science, pages 50--65. Springer, 2012. Google ScholarGoogle ScholarDigital LibraryDigital Library
  48. Project EVA. Security protocols open repository, 2007. http://www.lsv.ens-cachan.fr/spore/.Google ScholarGoogle Scholar
  49. A. Rial and G. Danezis. Privacy-friendly smart metering. Technical Report MSR-TR-2010-150, Microsoft Research, 2010.Google ScholarGoogle Scholar
  50. O. Udrea, C. Lumezanu, and J. S. Foster. Rule-Based static analysis of network protocol implementations. IN PROCEEDINGS OF THE 15TH USENIX SECURITY SYMPOSIUM, pages 193--208, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  51. D. Unruh. The impossibility of computationally sound XOR, July 2010. Preprint on IACR ePrint 2010/389.Google ScholarGoogle Scholar

Index Terms

  1. Computational verification of C protocol implementations by symbolic execution

    Recommendations

    Comments

    Login options

    Check if you have access through your login credentials or your institution to get full access on this article.

    Sign in
    • Published in

      cover image ACM Conferences
      CCS '12: Proceedings of the 2012 ACM conference on Computer and communications security
      October 2012
      1088 pages
      ISBN:9781450316514
      DOI:10.1145/2382196

      Copyright © 2012 ACM

      Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

      Publisher

      Association for Computing Machinery

      New York, NY, United States

      Publication History

      • Published: 16 October 2012

      Permissions

      Request permissions about this article.

      Request Permissions

      Check for updates

      Qualifiers

      • research-article

      Acceptance Rates

      Overall Acceptance Rate1,261of6,999submissions,18%

      Upcoming Conference

      CCS '24
      ACM SIGSAC Conference on Computer and Communications Security
      October 14 - 18, 2024
      Salt Lake City , UT , USA

    PDF Format

    View or Download as a PDF file.

    PDF

    eReader

    View online with eReader.

    eReader